/*  Francesco Cotto
 *  
 *  PDP
 *  
 *  Type Checker (inference) - prolog
 *      per miniml
 *
 */


%CONTESTO : contiene le variabili libere presenti nel termine

%typenv(Variabile,Contesto,Tipo)
typenv(X,[ass(X,Y)|_],Y).

%ricerca X di tipo Y nel contesto (scorrimento lista)
typenv(X,[_|Env],Y) :- typenv(X,Env,Y). 



%ASSIOMI

%tipi immediatamente derivabili
type(true,_,bool).
type(false,_,bool).

%numeri naturali (>=0) come successori di zero
type(num(0),_,int):-!.
type(num(X),_,int):- Y is X-1 , type(num(Y),_,int).

%operatori logici/matematici in forma curryficata
type(bfun(Op),_,arr(int,arr(int,int))) :- Op = + ; Op = - ; Op = * .
type(bfun(=),_,arr(int,arr(int,bool))).
type(bfun(=),_,arr(bool,arr(bool,bool))).
%

%aggiunta di una variabile al contesto 
type(var(X), Env, Y) :- typenv(X,Env,Y).

%Astrazione
type(fun(V,M),Env,arr(T,W)):- type(M,[ass(V,T)|Env],W).

%Applicazione
type(app(X,Y), Env, T) :- type(X,Env,arr(U1,T)), type(Y,Env,U2),
      unify_with_occurs_check(U1,U2).
/*type(app(X,Y), Env, T) :- type(X,Env,arr(U,T)), type(Y,Env,U).*/


%let Variabile = termine in termine2
%Let : come zucchero sintattico, uso della definizione
type(let(V,M1,M2),E,T):-type(app(fun(V,M2),M1),E,T).

%Let : regola di derivazione di tipo
/*type(let(X,T1,T2),E,T):-type(T1,E,TIPO1), type(T2,[ass(X,TIPO1)|E],T).*/


%Cond
type(cond(C,T,E),Env,Tif):-type(C,Env,bool) , type(T,Env,Tt), type(E,Env,Te),
        unify_with_occurs_check(Tt,Te) , Tif=Tt.

/*type(cond(C,T,E),Env,Tif):-type(C,Env,bool) , type(T,Env,Tif) , type(E,Env,Tif).*/


%ESEMPI DI TYPE INFERENCE E TYPE CHECKING
/* 

| ?- type(fun(x,var(x)),[],X).

X = arr(A,A) ? ;

| ?- type(app(fun(x,var(x)),num(_)),_,X).

X = int ? ;

| ?- type(let(x,num(3),fun(y,var(x))),_,X).

X = arr(_,int) ? ;

| ?- type(let(x,num(3),app(fun(y,var(y)),var(x))),_,X).

X = int ? 


| ?- type(let(x,num(3),var(x)),_,X).

X = int ? 


| ?- type(app(app(bfun(=),num(2)),num(6)),_,X).

X = bool

*/
